basic
\\[0ex]irrefl($T$;$R$) $\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$Irrefl($T$;$x$,$y$.$R$($x$,$y$))